COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	second[w87,jmc]		Notes on second order logic
C00006 ENDMK
C⊗;
second[w87,jmc]		Notes on second order logic

Second order logic and the model theory of first order logic.

How much of the model theory of a first order language can be
expressed in second order formulas with the same function and
predicate constants?  We can do circumscription but it appears
that we can't so readily do non-monotonic unique names.

We can also do Shoham's chronological minimization, i.e. what
he says in model-theoretic terms can be expressed as a second
order formula.  I argue that using second order logic is epistemologically
better than leaving a model-theoretic formulation.  If it is
left model-theoretic than a separate reasoning apparatus has
to be created on a meta-linguistic level.  This may be necessary
if intensional reasoning is required.  Shoham's chronological
minimization reasoning is not intensional and so can be
expressed as a second order extensional theory.  The examples
used by Reiter and Shoham and Bossu and Siegel are all involve
only a finite set of finite models.  Therefore, it is not difficult to
enumerate the models and do the computations.  If either the models
were infinite or even if there were an infinite set of finite models
that had to be considered, these computations with the models
would not be feasible by the methods used by these authors.
Then the second order formulations would be clearly preferable
even to the meanest intelligence.

It is interesting to ask when the expression of these other model
theoretic statements reduce to circumscription.  In the case of
chronological minimization, it isn't obvious how to do it.

Chronological minimization

	Suppose we have an axiom  A(Z)  involving predicate symbols
Z and there is a distinguished variable t included among the arguments
of some of the  Z's.  Now suppose there is
an ordering Z1(t) ≤ Z2(t) with  t  as a parameter.
We then define an ordering

Z1 ≤ Z2 ≡ Z1 = Z2 ∨ ∃t0.(∀t.(t < t0 ⊃ Z1(t) = Z2(t)) ∧ Z1(t0) < Z2(t0))

Asserting that  Z  is minimal in that ordering among  Z's  that
that satisfy  A(Z)  realizes chronological minimization as a second
order formula.  It is not obviously a circumscription.